This invention relates to computer software algorithms, specifically to reorganizing computing resources in the middle of checking whether a very complex Boolean function is a tautology with a given constraint.
The value of a Boolean function can be either 0 or 1. A Boolean function can depend on any number of variables, and each variable's value can be either 0 or 1. The Boolean function maps each combination of values of these variables to either 0 or 1. A Boolean function is satisfiable if it maps at least one such combination to 1. A Boolean function is a tautology if it maps all combinations to 1. A Boolean function is a tautology if and only if the negation of the Boolean function is not satisfiable.
A tautology checking method decides whether a given Boolean function is a tautology. An equivalence checking method decides whether two given Boolean functions are equivalent. An equivalence checking method can be used as a tautology checking method if one of the two given Boolean functions is Boolean constant 1. A tautology checking method can perform equivalence checking if the given Boolean function is the exclusive nor (XNOR) of two Boolean functions. A given Boolean function is a tautology if and only if it can be simplified to Boolean constant 1. It is sometimes possible to checking tautology for a simple Boolean function with traditional Boolean simplification methods such as applying Boolean simplification theorems and using Karnaugh maps. However, these Boolean simplification methods do not work with slightly complex tautology checking methods because their failure to simplify a Boolean function to a constant does not mean all other methods must also fail.
Because the value of a signal in a digital circuit can be either 1 or 0, digital circuits are often represented as Boolean functions. Equivalence checking methods, satisfiability checking methods and tautology checking methods can be used to check whether two digital circuits are equivalent, which is used in functional design verification of digital circuits. The verification is generally performed as checking the equivalence between a specification and an implementation. In addition to this equivalence, it is well known that these methods can be used to solve other properties of digital circuits in many areas of CAD such as automatic test pattern generation, verification, design error correction, synthesis, physical design, and others. These methods can be very useful when using computers to execute them.
As digital circuits become more and more complex while integrated circuit technologies grow, equivalence checking methods and tautology checking methods often fail to handle the complex Boolean functions used to represent digital circuits. The failures are either due to unreasonably long run times or due to requiring unreasonably large amounts of computer memory. These methods (such as U.S. Pat. No. 5,243,538 and others using BDDs) give meaningful conclusions only at the end, and therefore they give no meaningful conclusions at all if they fail before reaching the end. A truth table of a Boolean function involving 100 Boolean variables can fill more than 1000 trillion storage devices if each of such storage devices can store 1000 trillion rows of the truth table, which is much larger than most modern hard disks or tapes. Just touching such amount of data at the speed of 30 billion rows per second (faster than the modern speed of accessing registers) takes more than a trillion years per pass. It is well known that BDDs of many practical Boolean functions have sizes similar to these truth tables'. This amount of data is similar to the amount of data needed for any method listing the function's output values at all points in the input space. Therefore, any method involving the inspection of output values of a complex Boolean function is impractical if the function has more than 100 variables. Some of these methods are related to adjacency theorem.
A way to avoid such failures is to check equivalence or tautology for only some of all combinations of the variable values. This provides meaningful conclusions before the end of checking for all combinations of the variable values. This is used widely in the industry because each of the ignored combinations is often similar enough to a combination involved in the checking or some combinations are less critical than others. This is normally performed as logic simulation for one combination at a time. When the same combinations are involved, logic simulation is usually much less efficient than equivalence checking methods or tautology checking methods.
There clearly are needs of more efficient methods for checking equivalence or tautology for a given subset of all combinations of the variable values.